Inference at * 1 0 
Iof proof for Lemma absval ubound:



1. i : 
2. n : 
  (|i|  n)  (((-n)  i) & (i  n)) 

latex

 by PERMUTE{1:n,
 by PERMUTE{2:n,
 by PERMUTE{3:n,
 by PERMUTE{4:n,
 by PERMUTE{5:n,
 by PERMUTE{6:n,
 by PERMUTE{7:n,
 by PERMUTE{8:n,
 by PERMUTE{9:n,
 by PERMUTE{10:n,
 by PERMUTE{11:n,
 by PERMUTE{12:n,
 by PERMUTE{10:n,
 by PERMUTE{13:n,
 by PERMUTE{11:n,
 by PERMUTE{14:n,
 by PERMUTE{15:n,
 by PERMUTE{16:n,
 by PERMUTE{17:n,
 by PERMUTE{18:n,
 by PERMUTE{16:n,
 by PERMUTE{15:n,
 by PERMUTE{19:n} 

latex

 1: .....wf..... NILNIL

 1:   0 z i  
 2: .....wf..... NILNIL

 2:     Type
 3: .....wf..... NILNIL

 3: 3. 0 z i = tt
 3:   (0 z i = tt)  
 4: .....wf..... NILNIL

 4: 3. 0 z i = tt
 4:   (0 z i)  
 5: .....wf..... NILNIL

 5: 3. 0 z i = tt
 5:   (0  i)  
 6: .....wf..... NILNIL

 6: 3. 0 z i = tt
 6:   0 z i  
 7: .....wf..... NILNIL

 7: 3. 0 z i = tt
 7:   0  
 8: .....wf..... NILNIL

 8: 3. 0 z i = tt
 8:   i  
 9: .....truecase..... NILNIL

 9: 3. 0  i
 9:   (i  n)  (((-n)  i) & (i  n))
 10: .....wf..... NILNIL

 10: 3. 0 z i = ff
 10:   (0 z i = ff)  
 11: .....wf..... NILNIL

 11: 3. 0 z i = ff
 11:   (i <z 0)  
 12: .....wf..... NILNIL

 12: 3. 0 z i = ff
 12:   (i < 0)  
 13: .....wf..... NILNIL

 13: 3. 0 z i = ff
 13:   ((0 z i))  
 14: .....wf..... NILNIL

 14: 3. 0 z i = ff
 14:   0 z i  
 15: .....wf..... NILNIL

 15: 3. 0 z i = ff
 15:   0  
 16: .....wf..... NILNIL

 16: 3. 0 z i = ff
 16:   i  
 17: .....antecedent..... NILNIL

 17: 3. 0 z i = ff
 17:   True
 18: .....wf..... NILNIL

 18: 3. 0 z i = ff
 18: 4. ((0 z i)) = (i <z 0)
 18:    = 
 19: .....falsecase..... NILNIL

 19: 3. i < 0
 19:   ((-i)  n)  (((-n)  i) & (i  n))
 .

Definitions	{x:A| B(x)} , x.A(x), b, i <z j, a < b, inr x , case b of inl(x) => s(x) | inr(y) => t(y), x:A  B(x), b, f(a), , Ax, inl x , left + right, x:AB(x), s = t, Type, #$n, i z j, -n, A  B, , , , Unit, , True, T, ff, P  Q, tt, P  Q, x:A. B(x), t  T, if b then t else f fi , P & Q, |i|, P  Q
Lemmas	assert of lt int, bnot of le int, bool wf, true wf, squash wf, assert wf, eqff to assert, assert of le int, eqtt to assert, iff transitivity